| Definitions | P    Q, P Q, i <z j,   b, i  z j, nth_tl(n;as), False, A, A B, i j < k, Y, ||as||, {i..j }, l[i], hd(l), null(as),  x:A. B(x), {T}, SQType(T), tag(e), state@i, k(v:B) sends on l [tg:T, f <state, v>]?[], ff, DeclaredType(ds;x),   x. t(x), A c B, P & Q, tt,  , t  T, if b then t else f fi , P Q, Top, State(ds), IdLnk, a:A fp B(a), Knd,  x:A. B(x), i  j , P  Q, rcvs from e on l = L, isl(x), isrcv(k), p q, isrcvl(l;k),  b, as @ bs, reduce(f;k;as), concat(ll), t.2, t.1, sends-msgs(s;v;tg_f), map(f;as), e@i. P(e), sends k(v:T) on l:tagged(g,State(ds),v):dt, Unit, x(s),  ,  , x {FDLNOr12445} |
| Lemmas | map wf, nil member, es-val wf, non neg length, bool cases, member singleton, le wf, select member, es-sender wf, es-rcv-kind, Id sq, pi2 wf, pi1 wf, es-tag wf, fpf-dom wf, es-lnk wf, subtype rel list, length-map-sq, length wf1, bool sq, Knd sq, es-kind-rcv, subtype rel sum, es-state-subtype, es-vartype wf, subtype rel product, subtype rel function, can-apply wf, rcv wf, es-E wf, lsrc wf, es-loc wf, es-kind wf, Knd wf, fpf-cap-single1, fpf-single wf, lnk wf, isrcv wf, not functionality wrt iff, decl-type wf, fpf-cap wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, do-apply wf, fpf-cap-single-join, eqtt to assert, tagof wf, fpf-single wf3, fpf-join wf, sends-p wf, assert-isrcvl, bool wf, IdLnk wf, l member wf, Id wf, top wf, decl-state wf, event system wf |
vTyp)
es:ES.
tag(k) : vTyp else tg : mTyp fi